Nuprl Lemma : init_p-discrete
11,40
postcript
pdf
es
:ES,
i
,
x
:Id,
T
:Type,
v
:
T
.
(
discrete(
i
;
x
))
@
i
continuous
x
initially
t
.
v
:
T
@
i
x
initially
v
:
T
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
@
i
x
initially
v
:
T
,
A
c
B
,
@
i
(
x
:
T
)
,
P
&
Q
,
t
T
,
@
i
continuous
x
initially
v
:
T
,
Lemmas
init
p
wf
,
rationals
wf
,
assert
wf
,
es-isconst
wf
,
Id
wf
,
event
system
wf
origin
es:ES, i, x:Id, T:Type, v:T.
discrete(i;x)) 
@i continuous x initially 
t.v:T @i x initially v:T es:ES, i, x:Id, T:Type, v:T.
discrete(i;x)) @i continuous x initially t.v:T @i x initially v:T x:A. B(x) Q
B
T